\documentstyle[portrait,%
              fancybox,%
              notes,%
              epsfig,%
              alltt,%
              semcolor,
              alltt]{seminar}

\input amssym.def
\input amssym

\newcommand{\nat}{\mbox{$\protect\Bbb N$}}
\newcommand{\num}{\mbox{$\protect\Bbb Z$}}
\newcommand{\rat}{\mbox{$\protect\Bbb Q$}}
\newcommand{\real}{\mbox{$\protect\Bbb R$}}
\newcommand{\complex}{\mbox{$\protect\Bbb C$}}
\newcommand{\xxx}{\mbox{$\protect\Bbb X$}}

\newcommand{\lamb}[1]{\lambda #1.\:}
\newcommand{\eps}[1]{\varepsilon #1.\:}
\newcommand{\all}[1]{\forall #1.\:}
\newcommand{\ex}[1]{\exists #1.\:}
\newcommand{\exu}[1]{\exists! #1.\:}

\newcommand{\True}{\top}
\newcommand{\False}{\bot}
\newcommand{\Not}{\neg}
\newcommand{\And}{\wedge}
\newcommand{\Or}{\vee}
\newcommand{\Imp}{\Rightarrow}
\newcommand{\Iff}{\Leftrightarrow}

\newcommand{\entails}{\vdash}
\newcommand{\proves}{\vdash}

\newcommand{\Ands}{\bigwedge}
\newcommand{\Ors}{\bigvee}

\newcommand{\BQ}{\mbox{$\ulcorner$}}
\newcommand{\BEQ}{\mbox{\raise4pt\hbox{$\ulcorner$}}}
\newcommand{\EQ}{\mbox{$\urcorner$}}
\newcommand{\EEQ}{\mbox{\raise4pt\hbox{$\urcorner$}}}

\newcommand{\QUOTE}[1]{\mbox{$\BQ #1 \EQ$}}
\let\psubset=\subset                    % Pure TeX: thanks to MAJ %
\let\subset=\subseteq

\newcommand{\powerset}{\wp}             % This is pretty dire...  %

\newcommand{\Union}{\cup}
\newcommand{\Inter}{\cap}
\newcommand{\Unions}{\bigcup}
\newcommand{\Inters}{\bigcap}

\newcommand{\proof}{{\bf \noindent Proof:\ }}
\newcommand{\qed}{Q.E.D.}

\newcommand{\Rule}{\infer}

\newcommand{\restrict}{\upharpoonright} % This is lousy and must be fixed! %

\newcommand{\bigsqcap}{\mbox{\Large{$\sqcap$}}}

\newcommand\leb{\lbrack\!\lbrack}
\newcommand\reb{\rbrack\!\rbrack}
\newcommand{\sem}[1]{\leb #1 \reb}

\newcommand{\BA}{\begin{array}[t]{l}}
\newcommand{\EA}{\end{array}}
\newcommand{\sqle}{\sqsubseteq}
\newcommand{\sqlt}{\sqsubset}

\newcommand{\too}{\twoheadrightarrow}

\newcommand{\Los}{{\L}o{\'s}}

% These are from Mike's notes

\def\alphas{\mathrel{\mathop{\longrightarrow}\limits_{\alpha}}}
\def\betas{\mathrel{\mathop{\longrightarrow}\limits_{\beta}}}
\def\etas{\mathrel{\mathop{\longrightarrow}\limits_{\eta}}}

\def\goesto{\longrightarrow}

\newcommand{\defeq}{\stackrel{\bigtriangleup}{=}}

% Sizes

\renewcommand{\slidetopmargin}{0.8in}
\renewcommand{\slidebottommargin}{0.8in}

% Various combinations of one colour on another

\newcommand{\greenonred}[1]%
{\psset{fillcolor=red}\psframebox*[framearc=.3]{\green #1}}

\newcommand{\whiteonred}[1]%
{\psset{fillcolor=red}\psframebox*[framearc=.3]{\white #1}}

\newcommand{\yellowonmagenta}[1]%
{\psset{fillcolor=magenta}\psframebox*[framearc=.3]{\yellow #1}}

\newcommand{\whiteonblack}[1]%
{\psset{fillcolor=black}\psframebox*[framearc=.3]{\white #1}}

\newcommand{\blackonlightgray}[1]%
{\psset{fillcolor=lightgray}\psframebox*[framearc=.3]{\black #1}}

\newcommand{\blueonlightgray}[1]%
{\psset{fillcolor=lightgray}\psframebox*[framearc=.3]{\blue #1}}

\newcommand{\cyanonblack}[1]%
{\psset{fillcolor=black}\psframebox*[framearc=.3]{\cyan #1}}

\newcommand{\blueonyellow}[1]%
{\psset{fillcolor=yellow}\psframebox*[framearc=.3]{\blue #1}}

\newcommand{\redonyellow}[1]%
{\psset{fillcolor=yellow}\psframebox*[framearc=.3]{\red #1}}

\newcommand{\heading}[1]%
{\begin{center}\whiteonblack{\large\bf\blueonlightgray{#1}}\end{center}}

\newcommand{\emphatic}[1]{\blueonyellow{#1}}

\newcommand{\veryemphatic}[1]%
{\begin{center}{\emphatic{#1}}\end{center}}

% Head and foot of slides

\newpagestyle{ColourDemo}%
  {\cyanonblack{Introduction to Functional Programming:
                Lecture 4}\hfil\cyanonblack{\thepage}}
  {\cyanonblack{John Harrison}\hfil
   \cyanonblack{University of Cambridge, 23 January 1997}}

\pagestyle{ColourDemo}

\centerslidesfalse

% Colour bullets

\def\labelitemi{{\black$\bullet$}}
\def\labelitemii{{\black--}}
\def\labelitemiii{{\black$\ast$}}
\def\labelitemiv{{\black$\cdot$}}

% Start of document (default text colour is blue)

\begin{document}\blue


\begin{slide*}

\heading{%
\begin{tabular}{c}
{\LARGE\red Introduction to}\\
{\LARGE\red Functional Programming}\\
{\cyan John Harrison}\\
{\cyan University of Cambridge}\\
{\green Lecture 4}\\
{\green Types}
\end{tabular}}

\vspace*{0.1cm}

Topics covered:

\begin{itemize}

\item Why types? Answers from logic and programming

\item Simply typed lambda calculus

\item Polymorphism

\item Let polymorphism

\item Most general types and Milner's algorithm

\item Strong normalization; recursion.

\end{itemize}

\end{slide*}




\begin{slide*}

\heading{Logical reasons for types}

\vspace*{0.5cm}

Just what do the `terms' in $\lambda$-calculus really {\em mean}? How can it
make sense to apply a function to itself as in {\red $f\; f$}?

It makes some sense for functions like the identity {\red $\lamb{x} x$}
or constant functions {\red $\lamb{x} y$}. But in general it looks very
suspicious.

Perhaps this is why the attempt to extend the system to include set theory hit
Russell's paradox.

This is why Church developed typed lambda calculus, which is successfully used,
even to this day, as a foundation for mathematics.

Type theory is now seen as an {\em alternative} to set theory as a foundation.
There are interesting links between type theory and programming (Martin-L\"of
and others).

\end{slide*}




\begin{slide*}

\heading{Programming reasons for types}

\vspace*{0.5cm}

Types were introduced in programming for a mixture of reasons. We can (at least
in retrospect) see the following advantages:

\begin{itemize}

\item They can help the computer to generate more efficient code, and use space
more effectively.

\item They serve as a kind of `sanity check' for programs, catching a lot of
programming errors before execution.

\item They can serve as documentation for people.

\item They can help with data hiding and modularization.

\end{itemize}

At the same time, some programmers find them an irksome restriction. How can we
achieve the best balance?

\end{slide*}




\begin{slide*}

\heading{Different typing methods}

\vspace*{0.4cm}

We can distinguish between

\begin{itemize}

\item Strong typing, as in Modula-3, where types must match up exactly.

\item Weak typing, as in C, where greater latitude is allowed (e.g. an argument
of type {\tt int} to a function expecting a {\tt float}).

\end{itemize}

and also between

\begin{itemize}

\item Static typing, as in FORTRAN, which happens during compilation

\item Dynamic typing, as in LISP, which happens during execution.

\end{itemize}

ML is statically and strongly typed. At the same time, a feature called {\em
polymorphism} gives many benefits of weak or dynamic typing.

\end{slide*}


\begin{slide*}

\heading{The stock of types}

\vspace*{0.5cm}

For now, we assume that we have some set {\red $Ptys$} of type constants, e.g.
{\red \tt int} and {\red \tt bool}, and we can build up new types from them
using only the function type constructor, e.g.
{\red $$ \mbox{int} \to \mbox{int} $$}
and
{\red $$ (\mbox{int} \to \mbox{bool}) \to \mbox{int} \to \mbox{bool} $$}
(We assume that the function arrow is normally right-associative.)

Formally, this is another inductive definition.

In due course we will introduce more type constructors, e.g. the product type
{\red $\alpha \times \beta$}, as well as type {\em variables}, involved in
polymorphism. We normally use {\red $\alpha$} and {\red $\beta$} for type
variables.

\end{slide*}



\begin{slide*}

\heading{The idea of typed $\lambda$-calculus}

\vspace*{0.5cm}

Here we simply give every $\lambda$-term a {\em type}, and enforce
strong typing.

We can only form an application {\red $s\; t$} if the types match up, i.e.
{\red $s$} has function type {\red $\sigma \to \tau$} and {\red $t$} has type
{\red $\sigma$}. In that case, the combination {\red $s\; t$} has type {\red
$\tau$}.

We use the notation {\red $t:\sigma$} to mean `{\red $t$} has type {\red
$\sigma$}'.

We think of types as sets in which the objects denoted by terms live, and read
{\red $t:\sigma$} as {\red $t \in \sigma$}. This is the usual mathematical
notation in the case of function spaces.

However as usual, this interpretation is only a heuristic guide, and we develop
simply typed $\lambda$-calculus as a formal system.

\end{slide*}



\begin{slide*}

\heading{Church typing}

\vspace*{0.5cm}

This is a way of making the types part of the term structure. It is a system of
{\em explicit} types.

\begin{itemize}

\item Every constant {\red $c:\sigma_c$} is associated with a particular type.

\item A variable can have any type; identically-named variables with different
types are different terms.

\item If {\red $s:\sigma \to \tau$} and {\red $t:\sigma$} are terms, then
{\red $s\; t : \tau$} is a term.

\item If {\red $v:\sigma$} is a variable and {\red $t:\tau$} is a term then
{\red $\lamb{x} t : \sigma \to \tau$} is a term.

\end{itemize}

However we prefer to use {\em implicit} typing. In fact, in ML, the user never
has to write a type!

\end{slide*}



\begin{slide*}

\heading{Curry typing}

\vspace*{0.5cm}

Here the terms are exactly the same as before, and there is a separate notion
of typing. All typing is {\em implicit}, and a term may have many types. We use
a {\em context} {\red $\Gamma$} which gives type assignments for variables and
constants. Now:

{\red $$ \Gamma \vdash t : \sigma $$}

means that `assuming all the type assignments in {\red $\Gamma$} hold, then
{\red $t$} has type {\red $\sigma$}'.

We will continue to write simply {\red $t : \sigma$} in cases where the context
is empty.

\end{slide*}




\begin{slide*}

\heading{Formal typing rules}

\vspace*{0.5cm}

The typing relation is defined inductively as follows:

\begin{red}
$$ \frac{v:\sigma \in \Gamma}{\Gamma \vdash v : \sigma} $$

$$ \frac{c:\sigma \in \Gamma}{\Gamma \vdash c : \sigma} $$

$$ \frac{\Gamma \vdash s : \sigma \to \tau \;\;\;\ \Gamma \vdash t : \sigma}
        {\Gamma \vdash s\; t : \tau} $$

$$ \frac{\Gamma \Union \{v:\sigma\} \vdash t:\tau}
        {\Gamma \vdash \lamb{v} t : \sigma \to \tau} $$
\end{red}

\end{slide*}


\begin{slide*}

\heading{An example}

\vspace*{0.5cm}

Let us see how to assign a type to the identity function {\red $\lamb{x} x$}.
By the first rule we have:

{\red $$ \{x:\sigma\} \vdash x:\sigma $$}

and therefore by the last rule we get as expected

{\red $$ \emptyset \vdash \lamb{x} x : \sigma \to \sigma $$}

By convention, we just write {\red $\lamb{x} x : \sigma \to \sigma$}.

Note that the context was crucial to `link' different occurrences of the same
variable. In Church typing this would not have been needed as each variable
carries around its type.

\end{slide*}




\begin{slide*}

\heading{Type preservation}

\vspace*{0.5cm}

The conversion rules are exactly the same as in the untyped case.

A very important property is {\em type preservation}. This says that the
conversion rules from untyped $\lambda$-calculus preserve the typability
properties.

For example if {\red $\Gamma \vdash t : \sigma$} and {\red $t \betas t'$}, then
also {\red $\Gamma \vdash t' : \sigma$}.

Similar properties hold for the other conversions, and by structural induction
we find that if {\red $\Gamma \vdash t : \sigma$} and {\red $t \goesto t'$},
then also {\red $\Gamma \vdash t' : \sigma$}.

This shows that static typing and dynamic execution don't interfere with each
other.

\end{slide*}



\begin{slide*}

\heading{Adding new types}

\vspace*{0.5cm}

The above system still works if we add more primitive types and type
constructors.

For example, let us introduce a new binary type constructor {\red $\times$}
for product types.

We also introduce the (infix) pairing operator `{\red$,$}', which has type
{\red $\sigma \to \tau \to \sigma \times \tau$}. Thus:

{\red $$ (x:\sigma),(y:\tau) : \sigma \times \tau $$}

We can also introduce constants {\red $\mbox{fst}:\sigma \times \tau \to
\sigma$} and {\red $\mbox{snd}:\sigma \times \tau \to \tau$}.

In general, we can have arbitrarily many type constructors, and arbitrary
constants whose types involve these constructors. As we shall see, ML lets us
define our own type constructors.

\end{slide*}



\begin{slide*}

\heading{Polymorphism}

\vspace*{0.5cm}

The Curry typing system already gives us a form of {\em polymorphism}, in that
a given term may have different types. We distinguish between

\begin{itemize}

\item True (`parametric') polymorphism, where all the possible types bear a
structural relationship.

\item Ad hoc polymorphism, or {\em overloading}, where the different types a
term may have are different, e.g. the use of {\red $+$} over different number
systems.

\end{itemize}

We have true, parametric, polymorphism. For example, possible types for the
identity function are {\red $\sigma \to \sigma$}, {\red $\tau \to \tau$}, or
{\red $(\sigma \to \tau) \to (\sigma \to \tau)$}.

\end{slide*}



\begin{slide*}

\heading{Let polymorphism (1)}

\vspace*{0.5cm}

Our system has an unfortunate restriction. We can use the same expression with
different types in the same term, e.g:
{\red $$ \mbox{if}\; (\lamb{x} x)\; \mbox{true then}\; (\lamb{x} x)\; 1\;
\mbox{else}\; 0 $$}
However if we use a local {\tt let} binding, this is no longer the case.
Consider:
{\red $$ \mbox{let}\; I = \lamb{x} x\; \mbox{in if}\; I\; \mbox{true then}\; I
\; 1\; \mbox{else}\; 0 $$}
\noindent According to our definitions, this is just syntactic sugar for:
{\red $$ (\lamb{I} \mbox{if}\; I\; \mbox{true then}\; I \; 1\; \mbox{else}\;
0)\; (\lamb{x} x) $$}
This cannot be typed according to our rules, since the {\em single} instance of
the identity function needs to be given a {\em single} type.

\end{slide*}



\begin{slide*}

\heading{Let polymorphism (2)}

\vspace*{0.5cm}

This restriction is unbearable for practical functional programming. We take
two measures to avoid it.

First, we make the {\tt let} construct {\em primitive}, instead of regarding it
as syntactic sugar, as before.

Secondly, we add a new typing rule:

{\red $$ \frac{\Gamma \vdash s : \sigma \;\;\; \Gamma \vdash t[s/x] : \tau}
        {\Gamma \vdash \mbox{let}\; x = s\; \mbox{in}\; t : \tau} $$}

Now we can type expressions like the above in the way that we would expect.

\end{slide*}



\begin{slide*}

\heading{Most general types (1)}

\vspace*{0.5cm}

We have said that the different types for a term bear a structural similarity.
In fact more is true: there is always a {\em most general type} and all other
types are instances of this type.

We say that a type {\red $\sigma$} is more general than {\red $\sigma'$}, and
write {\red $\sigma \leq \sigma'$}, when we can substitute types for type
variables in {\red $\sigma$} and get {\red $\sigma'$}.

The formal definition of substitution at the type level is straightforward,
because there is no notion of binding. We will use the same notation. For
example:
{\red $$ \alpha \to bool \leq (\tau \to \tau) \to bool $$}
because
{\red $$ (\alpha \to bool)[(\tau \to \tau)/\alpha] = (\tau \to \tau)
\to bool $$}
But not conversely.


\end{slide*}


\begin{slide*}

\heading{Most general types (2)}

\vspace*{0.5cm}

Every expression in ML that has a type has a most general type. This was first
proved in a similar context by Hindley, and for the exact setup here by Milner.

What's more, there is an algorithm for finding the most general type of any
expression, even if it contains no type information at all.

ML implementations use this algorithm. Therefore it is never necessary in ML to
write down a type. All typing is implicit.

Thus, the ML type system is much less irksome than in many languages like
Modula-3. We never have to specify types explicitly {\em and} we can often
re-use the same code with different types: the compiler will work everything
out for us.

\end{slide*}



\begin{slide*}

\heading{Strong normalization}

\vspace*{0.5cm}

Recall our examples of terms with no normal form, such as:

\begin{red}
\begin{eqnarray*}
& & ((\lamb{x} x\; x\; x)\;(\lamb{x} x\; x\; x))     \\
& \goesto & ((\lamb{x} x\; x\; x)\;(\lamb{x} x\; x\; x)\;
                            (\lamb{x} x\; x\; x))                           \\
& \goesto & (\cdots)
\end{eqnarray*}
\end{red}
In typed lambda calculus, this cannot happen --- every typable term has a
normal form and all reduction sequences terminate in that normal form. This
property is known as {\em strong normalization}.

This sounds good --- every program terminates. Unfortunately this means that we
can't write all computable functions, or even all the interesting ones. We need
to add something.

\end{slide*}



\begin{slide*}

\heading{Recursion}

\vspace*{0.5cm}

We can't define arbitrary recursive functions any more --- if we could then we
could create non-terminating functions.

Clearly {\red $Y = \lamb{f} (\lamb{x} f(x\; x)) (\lamb{x} f(x\; x))$} isn't
well-typed because it applies {\red $x$} to itself.

So we simply add a way of defining arbitrary recursive functions that {\em is}
well-typed.

Introduce a family of polymorphic recursion operators of the form:

{\red $$ Rec : ((\alpha \to \beta) \to (\alpha \to \beta)) \to \alpha \to \beta
$$}

and the extra reduction rule that for any {\red $F:(\sigma \to \tau) \to
(\sigma \to \tau)$} we have:

{\red $$ Rec\; F \goesto F\; (Rec\;  F) $$}

\end{slide*}


\end{document}
